(set-logic QF_UFNRA)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const r3 Real)
(declare-const r8 Real)
(declare-const r9 Real)
(declare-const r10 Real)
(declare-const r12 Real)
(declare-const v6 Bool)
(declare-const r13 Real)
(declare-const v7 Bool)
(assert (or v6 v0 v0 v0 v3 v2 (xor v3 v5 v3 v0 v1 v0 v1 v2 (distinct 9321706.0 r8 r9) v2)))
(declare-const v9 Bool)
(declare-const v10 Bool)
(assert (= v9 v7 v5 v5 (distinct 9321706.0 r8 r9) (<= (/ r9 r8) 6399730.0 (/ r9 r8) r12) (= v6 v3 v4 (or v6 v0 v0 v0 v3 v2 (xor v3 v5 v3 v0 v1 v0 v1 v2 (distinct 9321706.0 r8 r9) v2))) (<= (/ r9 r8) 6399730.0 (/ r9 r8) r12) v10 (or v6 v0 v0 v0 v3 v2 (xor v3 v5 v3 v0 v1 v0 v1 v2 (distinct 9321706.0 r8 r9) v2)) v10))
(check-sat-assuming-model (r0 r1 r3 r8 r9 r10 r12 r13 ) (949766276.0 595769020.0 0.9323098753 2.0 890951084.0 0.097409118 9205131286.0 656.0 ))
